\begin{tabbing}
$\forall$${\it es}$:ES, $i$:Id, $L$:(IdLnk List), $T$:(Id$\rightarrow$Type).
\\[0ex]es{-}secret{-}server\=\{table:ut2, encrypt:ut2, decrypt:ut2\}\+
\\[0ex](${\it es}$; $T$; $L$; $i$)
\-\\[0ex]$\Rightarrow$ \=($\forall$$e_{1}$, $e_{2}$:E.\+
\\[0ex]($\exists$$l$$\in$$L$.kind($e_{1}$) = rcv(lnk{-}inv($l$),"encrypt") $\in$ Knd)
\\[0ex]$\Rightarrow$ ($\exists$$l$$\in$$L$.kind($e_{2}$) = rcv(lnk{-}inv($l$),"encrypt") $\in$ Knd)
\\[0ex]$\Rightarrow$ ((val($e_{1}$).2) = (val($e_{2}$).2) $\in$ Atom1)
\\[0ex]$\Rightarrow$ ($e_{1}$ = $e_{2}$))
\-
\end{tabbing}